E, X1, X2:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), pred?:(E(E+Unit)),
info:(E(IdX1+(IdLnkE)X2)),
p:(e:E, l:IdLnk.
p:(e':E.
p:(e'':E.
p:(rcv?(e'')
p:( sender(e'') = e
p:( link(e'') = l
p:( e'' = e'  e'' < e' & loc(e') = destination(l)  Id).
SWellFounded(pred!(e;e'))
 (e:E. first(e)  loc(pred(e)) = loc(e)  Id)
 (e, e':E. loc(e) = loc(e')  Id  pred?(e) = pred?(e')  e = e')
 (e:E, l:IdLnk, n:||receives(dE;dL;pred?;info;p;e;l)||.
 (e':E. rcv?(e') & link(e') = l & sender(e') = e & index(dE;dL;pred?;info;p;e') = n  ) 

latex

Definitions

sends-bound(p;e;l), eventlist(pred?;e), x before y  l, Dec(P), x. t(x), {T}, x f y, WellFnd{i}(A;x,y.R(x;y)), P  Q, eqof(d), S  T, , index(dE;dL;pred?;info;p;r), P  Q, SqStable(P), T, True, l[i], AB, i  j < k, , SWellFounded(R(x;y)), A & B, A, b, first(e), pred(e), EqDecider(T), x:A. B(x), rcv?(e), sender(e), link(e), P & Q, P  Q, e < e', destination(l), x,y. t(x;y), pred!(e;e'), Id, loc(e), Unit, Prop, IdLnk, {i..j}, ||as||, rcv-from-on(dE;dL;info;e;l;r), receives(dE;dL;pred?;info;p;e;l), t  T, x:A. B(x), False, P  Q

Lemmas

receives wf, rcv-from-on wf, assert wf, length wf1, int seg wf, unit wf, loc wf, Id wf, pred wf, first wf, not wf, pred! wf, strongwellfounded wf, ldst wf, cless wf, link wf, sender wf, rcv? wf, IdLnk wf, deq wf, nat wf, select wf, decidable assert, sq stable from decidable, assert-rcv-from-on, index wf, sq stable equal, sq stable and, eqof wf, le wf, mu-bound-unique, squash wf, true wf, deq property, rel plus strongwellfounded, strongwf-implies, decidable lt, l before wf, l before select, sends-bound wf, l before eventlist, eventlist wf, l before filter